p:FinProbSpace, S:((Outcome)). nullset(p;S)   

latex

Definitions	FinProbSpace, t  T, Type, , x:A. B(x), Outcome, , x:AB(x), measure(C)  q, s  C, f(a), P  Q, x:A  B(x), P & Q, p-open(p), x:A. B(x), , #$n, r < s, , {x:A| B(x)} , nullset(p;S)
Lemmas	rationals wf, qless wf, int inc rationals, p-open wf, p-open-member wf, p-measure-le wf, nat wf, p-outcome wf, finite-prob-space wf